A:Type, eq:EqDecider(A), f:a:A fp Top, x:A. x  dom(f)  (x  1of(f)) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), Top, (x  l), x. t(x), 1of(t), P  Q, P  Q, P & Q, P  Q, deq-member(eq;x;L), b, Prop, x  dom(f), a:A fp B(a)
Lemmas	all functionality wrt iff, iff functionality wrt iff, assert-deq-member, iff wf, assert wf, deq-member wf, pi1 wf, l member wf, top wf, deq wf